import network.Device;
import network.Network;
import network.Port;
import network.Rule;
import networkLoader.FBNetwork;
import verifier.JiffyVerifier;
import verifier.Ports.PersistentPorts;
import verifier.util.Changes;

import java.util.ArrayList;

public class TestContract {
    public static void main(String[] args) {
        SswContract();
        FswContract();
    }

    public static void SswContract() {
        Network n = FBNetwork.getNetwork();
        ArrayList<Rule> contractRules = new ArrayList<>();
        for (int iSpine = 0; iSpine < 4; iSpine++) {
            for (int iSsw = 0; iSsw < 48; iSsw++) {
                Device ssw = n.getDevice("ssw-"+iSpine+"-"+iSsw);
                for (int iPod = 0; iPod < 112; iPod++) {
                    Rule rule = new Rule(ssw, (iPod << 24), 8, ssw.getPort(ssw.getName() + ">" + "fsw-"+iPod+"-"+iSpine));
                    contractRules.add(rule);
                }
            }
        }
        JiffyVerifier verifier = new JiffyVerifier(n, new PersistentPorts());
        Changes changes = verifier.insertMiniBatch(contractRules);
        changes.aggrBDDs();
        verifier.update(changes);
        System.out.println("#contract on ssw #contract: " + contractRules.size());
        System.out.println("#contract on ssw #ECs: " + verifier.predSize());
    }

    public static void FswContract() {
        Network n = FBNetwork.getNetwork();
        ArrayList<Rule> contractRules = new ArrayList<>();
        for (int iPod = 0; iPod < 112; iPod++) {
            for (int iFsw = 0; iFsw < 4; iFsw++) {
                Device fsw = n.getDevice("fsw-" + iPod + "-" + iFsw);
                Port port = fsw.addPort(fsw.getName() + ">" + "spine");
                for (int iPod1 = 0; iPod1 < 112; iPod1++) {
                    if (iPod != iPod1) {
                        Rule rule = new Rule(fsw, (iPod1 << 24), 8, port);
                        contractRules.add(rule);
                    }
                }
            }
        }
        JiffyVerifier verifier = new JiffyVerifier(n, new PersistentPorts());
        Changes changes = verifier.insertMiniBatch(contractRules);
        changes.aggrBDDs();
        verifier.update(changes);
        System.out.println("#contract on fsw #contract: " + contractRules.size());
        System.out.println("#contract on fsw #ECs: " + verifier.predSize());
    }
}
